Inference at * 
Iof proof for Lemma member-exists2:


  T:Type, L:(T List). (x:T. (x  L))  (0 < ||L||) 

latex

 by InteriorProof ((((UnivCD) 
THENM (((RWO "member-exists" 0) 
THENM (RWO "length_of_not_nil" 0))
THENM (RWO "length_))) 
TCollapseTHEN (Auto)) 

latex

TC.

Definitions	x:A. B(x), (x  l), #$n, ||as||, A, s = t, x:A. B(x), type List, Type, P  Q, P & Q, x:A  B(x), P  Q, P  Q, x:AB(x), a < b, i  j , A  B
Lemmas	l member wf, member-exists, not wf, iff functionality wrt iff, length of not nil, iff wf, rev implies wf, ge wf